Failed to solve the following constraints:
  Is empty: unit2 ≅ unit1
      [ at Issue292c.agda:41,19-21 ]
